Miscellaneous bugfixes #23

Technius · 2023-12-11T02:07:30Z

This pull request includes several miscellaneous bugfixes, which (I think) should not introduce any breaking changes:

Fix a gcc -Wreturn-type warning in PowersetAbstractDomain and SmallSortedSetAbstractDomain that causes build failures in downstream projects compiled with -Werror -Wall.
Don't add test targets if the CMake variable BUILD_TESTING is falsey.
Fix the exported CMake sparta target using the wrong directory as the include directory when installed

Technius · 2023-12-11T02:15:25Z

I noticed the -Wreturn-type warning also appeared in SmallSortedSetAbstractDomain::contains(), so I have fixed the warning there as well.

arnaudvenet · 2023-12-11T03:46:35Z

These changes look good to me. @arthaud : you might want to double check the CMake changes. Thanks!

arthaud · 2023-12-11T11:45:27Z

include/sparta/PowersetAbstractDomain.h

+    SPARTA_ASSERT(false && "unknown AbstractValueKind");
+    // Return false to suppress -Wreturn-type warning reported by gcc
+    return false;


I'm curious to see if a different compiler that understands the switch case always returns would give a warning here mentioning that this is dead code
We will see what our CI says.

clang 16 does not raise any warnings here with -Wall -Wextra, although I have not tried MSVC.

test/CMakeLists.txt

arthaud · 2023-12-11T11:51:01Z

CMakeLists.txt

@@ -27,7 +28,7 @@ add_library(sparta INTERFACE)

 target_include_directories(sparta INTERFACE
      $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>
-      $<INSTALL_INTERFACE:include>
+      $<INSTALL_INTERFACE:${CMAKE_INSTALL_INCLUDEDIR}/sparta>


Are you sure about this?
I tried locally and this doesn't install correctly:

$ mkdir build $ cd build $ cmake -DCMAKE_INSTALL_PREFIX="../install" -DBUILD_TESTING=OFF .. $ make $ make install Install the project... -- Install configuration: "Release" -- Installing: /var/folders/28/bsnpkw693dj4g4r70vb7zn8m0000gn/T/tmp.r5N68DnBSw/SPARTA/install/include/sparta -- Installing: /var/folders/28/bsnpkw693dj4g4r70vb7zn8m0000gn/T/tmp.r5N68DnBSw/SPARTA/install/include/sparta/sparta -- Installing: /var/folders/28/bsnpkw693dj4g4r70vb7zn8m0000gn/T/tmp.r5N68DnBSw/SPARTA/install/include/sparta/sparta/HashedAbstractEnvironment.h -- Installing: /var/folders/28/bsnpkw693dj4g4r70vb7zn8m0000gn/T/tmp.r5N68DnBSw/SPARTA/install/include/sparta/sparta/PatriciaTreeMapAbstractPartition.h [...]

As you see, it installs under include/sparta/sparta, this is wrong.
This is with cmake 3.28.0 (installed with homebrew) on macOS.

This patch should only change the include directory attached to the generated sparta_targets.cmake. If the installed location is wrong, that is unrelated to this PR.

(Edit: I did not want to change the installed location to avoid breaking existing build configurations in other projects)

At least when I try it, the current behavior on main branch is consistent with what you are seeing:

$ cmake -B build -GNinja $ cmake --install build --prefix $(mktemp -d) -- Install configuration: "Release" -- Installing: /tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/include/sparta -- Installing: /tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/include/sparta/sparta -- Installing: /tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/include/sparta/sparta/AbstractDomain.h -- Installing: /tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/include/sparta/sparta/PatriciaTreeKeyTrait.h -- Installing: /tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/include/sparta/sparta/LiftedDomain.h [...] -- Installing: /tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/cmake/sparta_target.cmake

If you then inspect the contents of sparta_target.cmake, you'll see:

get_filename_component(_IMPORT_PREFIX "${CMAKE_CURRENT_LIST_FILE}" PATH) get_filename_component(_IMPORT_PREFIX "${_IMPORT_PREFIX}" PATH) if(_IMPORT_PREFIX STREQUAL "/") set(_IMPORT_PREFIX "") endif() # Create imported target sparta add_library(sparta INTERFACE IMPORTED) set_target_properties(sparta PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${_IMPORT_PREFIX}/include" INTERFACE_LINK_LIBRARIES "Boost::thread" )

So the INTERFACE_INCLUDE_DIRECTORIES would point to /tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/include, which wouldn't be right (it should point to include/sparta instead).

I confirmed this by generating a dummy CMake project:

$ cd $(mktemp -d) $ cat > CMakeLists.txt <<EOF cmake_minimum_required(VERSION 3.20) project(Example) find_package(Boost REQUIRED COMPONENTS thread) include("/tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/cmake/sparta_target.cmake") add_executable(example example.cpp) target_link_libraries(example PRIVATE sparta) EOF $ cat > example.cpp <<EOF #include <sparta/PowersetAbstractDomain.h> int main() { return 0; } EOF $ cmake -B build -GNinja $ cmake --build build /nix/store/90h6k8ylkgn81k10190v5c9ldyjpzgl9-gcc-wrapper-12.3.0/bin/g++ -DBOOST_THREAD_DYN_LINK -DBOOST_THREAD_NO_LIB -isystem /tmp/nix-shell.4NHxoh/tmp.8Eye3UvBMT/include -MD -MT CMakeFiles/example.dir/example.cpp.o -MF CMakeFiles/example.dir/example.cpp.o.d -o CMakeFiles/example.dir/example.cpp.o -c /tmp/nix-shell.4NHxoh/tmp.43SeFBEwQS/example.cpp /tmp/nix-shell.4NHxoh/tmp.43SeFBEwQS/example.cpp:1:10: fatal error: sparta/PowersetAbstractDomain.h: No such file or directory 1 | #include <sparta/PowersetAbstractDomain.h> | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ compilation terminated. ninja: build stopped: subcommand failed.

With this patch, the dummy project builds successfully instead.

I see. I do think we want to change this and force users to include <sparta/XXX> instead of <XXX> directly.
Let me try to make that change internally, then you can rebase on top of it?

Thanks. I've updated the include directories to be consistent with the new install location, and I've modified the commit message accordingly.

arthaud · 2023-12-13T08:27:06Z

LGTM

facebook-github-bot · 2023-12-13T08:27:44Z

@arthaud has imported this pull request. If you are a Meta employee, you can view this diff on Phabricator.

arthaud · 2023-12-13T12:04:21Z

include/sparta/PowersetAbstractDomain.h

@@ -235,6 +235,9 @@ class PowersetAbstractDomain
      return this->get_value()->contains(e);
    }
    }
+    SPARTA_ASSERT(false && "unknown AbstractValueKind");


We need to include:

#include <sparta/Exceptions.h>

Otherwise we are getting the error:

xxx/sparta/PowersetAbstractDomain.h:238:5: error: use of undeclared identifier 'assert' SPARTA_ASSERT(false && "unknown AbstractValueKind"); ^

arthaud · 2023-12-13T12:04:57Z

test/CMakeLists.txt

@@ -0,0 +1,12 @@
+file(GLOB test "*.cpp")


Please add our license header

# Copyright (c) Meta Platforms, Inc. and affiliates. # # This source code is licensed under the MIT license found in the # LICENSE file in the root directory of this source tree.

Always return false in PowersetAbstractDomain::contains() and SmallSortedSetAbstractDomain::contains() to avoid a gcc warning. On debug builds, this will instead trigger an assertion failure.

This commit ensures that test targets are only added if BUILD_TESTING is enabled when generating the CMake configuration. There should be no change in behavior, as BUILD_TESTING defaults to ON.

Currently, the sparta target will use `$CMAKE_INSTALL_PREFIX/include` as the include directory when installed. If the user sets a custom CMAKE_INSTALL_INCLUDEDIR, however, then this will not be the correct location. This commit changes the include directory of the sparta target to be consistent with the actual installed location.

facebook-github-bot · 2023-12-14T06:30:24Z

@Technius has updated the pull request. You must reimport the pull request before landing.

facebook-github-bot · 2023-12-14T09:46:36Z

@arthaud has imported this pull request. If you are a Meta employee, you can view this diff on Phabricator.

Summary: This pull request includes several miscellaneous bugfixes, which (I think) should not introduce any breaking changes: * Fix a gcc `-Wreturn-type` warning in `PowersetAbstractDomain` and `SmallSortedSetAbstractDomain` that causes build failures in downstream projects compiled with `-Werror -Wall`. * Don't add test targets if the CMake variable `BUILD_TESTING` is falsey. * Fix the exported CMake `sparta` target using the wrong directory as the include directory when installed X-link: facebook/SPARTA#23 Reviewed By: arnaudvenet Differential Revision: D52111351 Pulled By: arthaud fbshipit-source-id: 97d9a89537ce77f575f0e073b43f5d81eeba6a08

facebook-github-bot · 2023-12-15T10:44:17Z

@arthaud merged this pull request in f2f42d0.

Summary: This pull request includes several miscellaneous bugfixes, which (I think) should not introduce any breaking changes: * Fix a gcc `-Wreturn-type` warning in `PowersetAbstractDomain` and `SmallSortedSetAbstractDomain` that causes build failures in downstream projects compiled with `-Werror -Wall`. * Don't add test targets if the CMake variable `BUILD_TESTING` is falsey. * Fix the exported CMake `sparta` target using the wrong directory as the include directory when installed X-link: facebook/SPARTA#23 Reviewed By: arnaudvenet Differential Revision: D52111351 Pulled By: arthaud fbshipit-source-id: 97d9a89537ce77f575f0e073b43f5d81eeba6a08

Summary: This PR includes some improvements to the CMake configuration that makes SPARTA easier to use as a dependency (or at least I've found these useful for a project I'm working on). Specifically: * Generate a `sparta-config.cmake` file that is created in both the build folder and for the install target. This enables the library to be used with `find_package`. * (Breaking change) Install the `sparta_target.cmake` to `$LIBDIR/cmake/sparta` instead of `$PREFIX/cmake` to support \*nix systems as well as `find_package`. While this is a breaking change, it's unlikely that anyone used the installed file due to the bugs observed in facebook/SPARTA#23. * (Breaking change) Use `sparta::` as the target namespace when exporting the `sparta` target. Projects that previously included the `sparta_target.cmake` will need to be updated to use `sparta::sparta` instead of `sparta` when specifying it as a dependency. * Update the README with additional tips on how to use SPARTA in CMake projects. This PR is stacked on top of facebook/SPARTA#23, and I'll rebase after it is merged. X-link: facebook/SPARTA#24 Reviewed By: arnaudvenet Differential Revision: D52238117 Pulled By: arthaud fbshipit-source-id: abfad1312d5357a5adc64335d7a51e80935cf111

Summary: This PR includes some improvements to the CMake configuration that makes SPARTA easier to use as a dependency (or at least I've found these useful for a project I'm working on). Specifically: * Generate a `sparta-config.cmake` file that is created in both the build folder and for the install target. This enables the library to be used with `find_package`. * (Breaking change) Install the `sparta_target.cmake` to `$LIBDIR/cmake/sparta` instead of `$PREFIX/cmake` to support \*nix systems as well as `find_package`. While this is a breaking change, it's unlikely that anyone used the installed file due to the bugs observed in #23. * (Breaking change) Use `sparta::` as the target namespace when exporting the `sparta` target. Projects that previously included the `sparta_target.cmake` will need to be updated to use `sparta::sparta` instead of `sparta` when specifying it as a dependency. * Update the README with additional tips on how to use SPARTA in CMake projects. This PR is stacked on top of #23, and I'll rebase after it is merged. Pull Request resolved: #24 Reviewed By: arnaudvenet Differential Revision: D52238117 Pulled By: arthaud fbshipit-source-id: abfad1312d5357a5adc64335d7a51e80935cf111

Summary: This PR includes some improvements to the CMake configuration that makes SPARTA easier to use as a dependency (or at least I've found these useful for a project I'm working on). Specifically: * Generate a `sparta-config.cmake` file that is created in both the build folder and for the install target. This enables the library to be used with `find_package`. * (Breaking change) Install the `sparta_target.cmake` to `$LIBDIR/cmake/sparta` instead of `$PREFIX/cmake` to support \*nix systems as well as `find_package`. While this is a breaking change, it's unlikely that anyone used the installed file due to the bugs observed in facebook/SPARTA#23. * (Breaking change) Use `sparta::` as the target namespace when exporting the `sparta` target. Projects that previously included the `sparta_target.cmake` will need to be updated to use `sparta::sparta` instead of `sparta` when specifying it as a dependency. * Update the README with additional tips on how to use SPARTA in CMake projects. This PR is stacked on top of facebook/SPARTA#23, and I'll rebase after it is merged. X-link: facebook/SPARTA#24 Reviewed By: arnaudvenet Differential Revision: D52238117 Pulled By: arthaud fbshipit-source-id: abfad1312d5357a5adc64335d7a51e80935cf111

facebook-github-bot added the CLA Signed Do not delete this pull request or issue due to inactivity. label Dec 11, 2023

Technius force-pushed the bugfixes branch from 002c520 to e037789 Compare December 11, 2023 02:14

arnaudvenet self-assigned this Dec 11, 2023

arnaudvenet requested review from arnaudvenet and arthaud December 11, 2023 03:41

arthaud requested changes Dec 11, 2023

View reviewed changes

Technius force-pushed the bugfixes branch 2 times, most recently from 847beaf to 2ec9476 Compare December 13, 2023 04:07

arthaud requested changes Dec 13, 2023

View reviewed changes

Technius added 3 commits December 13, 2023 22:30

Fix GCC -Wreturn-type warnings

fdbef97

Always return false in PowersetAbstractDomain::contains() and SmallSortedSetAbstractDomain::contains() to avoid a gcc warning. On debug builds, this will instead trigger an assertion failure.

Only add test targets if testing is enabled

e5d1dbc

This commit ensures that test targets are only added if BUILD_TESTING is enabled when generating the CMake configuration. There should be no change in behavior, as BUILD_TESTING defaults to ON.

Technius force-pushed the bugfixes branch from 2ec9476 to 4b617ae Compare December 14, 2023 06:30

Technius mentioned this pull request Dec 14, 2023

Improvements to make SPARTA easier to use as a dependency #24

Closed

facebook-github-bot closed this in f2f42d0 Dec 15, 2023

facebook-github-bot added the Merged label Dec 15, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Miscellaneous bugfixes #23

Miscellaneous bugfixes #23

Technius commented Dec 11, 2023 •

edited

Loading

Technius commented Dec 11, 2023

arnaudvenet commented Dec 11, 2023 •

edited

Loading

arthaud Dec 11, 2023

Technius Dec 12, 2023

arthaud Dec 11, 2023 •

edited

Loading

Technius Dec 12, 2023 •

edited

Loading

arthaud Dec 12, 2023

Technius Dec 13, 2023

arthaud commented Dec 13, 2023

facebook-github-bot commented Dec 13, 2023

arthaud Dec 13, 2023

Technius Dec 14, 2023

arthaud Dec 13, 2023

Technius Dec 14, 2023

facebook-github-bot commented Dec 14, 2023

facebook-github-bot commented Dec 14, 2023

facebook-github-bot commented Dec 15, 2023

Miscellaneous bugfixes #23

Miscellaneous bugfixes #23

Conversation

Technius commented Dec 11, 2023 • edited Loading

Technius commented Dec 11, 2023

arnaudvenet commented Dec 11, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arthaud Dec 11, 2023 • edited Loading

Choose a reason for hiding this comment

Technius Dec 12, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arthaud commented Dec 13, 2023

facebook-github-bot commented Dec 13, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

facebook-github-bot commented Dec 14, 2023

facebook-github-bot commented Dec 14, 2023

facebook-github-bot commented Dec 15, 2023

Technius commented Dec 11, 2023 •

edited

Loading

arnaudvenet commented Dec 11, 2023 •

edited

Loading

arthaud Dec 11, 2023 •

edited

Loading

Technius Dec 12, 2023 •

edited

Loading